| Definitions |  x:A. B(x), Id, P   Q, ecl-trans-type(A), "$x", ecl-machine1{$ecl:ut2}(i; ds; da; A), ecl-machine2(i;ds;da;x;T;ks;a;upd), ecl-trans-ks(v), ecl-trans-a(v), let a,b,c,d,e,f,g = u in v(a;b;c;d;e;f;g), R-state-var-init(i;ds;da;x;T;v;ks;tr), t  T, 1of(t), Prop,   x. t(x),  A, A || B, R-state-var(i;ds;da;x;T;ks;tr), if b t else f fi, P & Q, Top, A & B, SQType(T), {T}, DeclaredType(ds;x), true, Y, Rplus?(x1), Rplus-left(x1), Rplus-right(x1), Rnone?(x1), True, R-loc(R), Rds(R), Rda(R), p = q, R-base-domain(R), R-frame-compat(A;B), R-interface-compat(A;B), p  q, i=j, 2of(t), Reffect?(x1), Rframe?(x1), Rframe-x(x1), Reffect-x(x1), Reffect-knd(x1), Rframe-L(x1), Raframe?(x1), Raframe-k(x1), Raframe-L(x1), Rrframe?(x1), Rrframe-x(x1), Reffect-ds(x1), Rrframe-L(x1), Rsends?(x1), Rsframe?(x1), Rsframe-lnk(x1), Rsends-l(x1), Rsframe-tag(x1), Rsends-g(x1), Rsends-knd(x1), Rsframe-L(x1), Rbframe?(x1), Rbframe-k(x1), Rbframe-L(x1), Rsends-ds(x1), Rpre?(x1), Rpre-ds(x1), Rpre-a(x1), Rsends-dt(x1), Reffect-T(x1), Rsends-T(x1), false, State(ds), f(x)?z, x,y. t(x;y), P  Q, P Q, P  Q, ecl-trans-tuple{i:l}(ds;da), x(s), update-spec-decl(upd;ds), Valtype(da;k),  , False, Unit, update-spec(ds;da), x(s1,s2),  , a = b |
Type, da:k:Knd fp